1 /-
2 Copyright (c) 2019 Floris van Doorn. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Floris van Doorn
5 -/
6
7 import analysis.complex.exponential
src └──────────────────────────┘
8
9 namespace real
10 variable (x : ℝ)
11
12 /-- the series `sqrt_two_add_series x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots,
13 starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2`
14 -/
15 @[simp] noncomputable def sqrt_two_add_series (x : ℝ) : ℕ → ℝ
doc └──┘
16 | 0 := x
17 | (n+1) := sqrt (2 + sqrt_two_add_series n)
18
19 lemma sqrt_two_add_series_zero : sqrt_two_add_series x 0 = x := by simp
20 lemma sqrt_two_add_series_one : sqrt_two_add_series 0 1 = sqrt 2 := by simp
21 lemma sqrt_two_add_series_two : sqrt_two_add_series 0 2 = sqrt (2 + sqrt 2) := by simp
22
23 lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), sqrt_two_add_series 0 n ≥ 0
24 | 0 := le_refl 0
25 | (n+1) := sqrt_nonneg _
26
27 lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), sqrt_two_add_series x n ≥ 0
28 | 0 := h
29 | (n+1) := sqrt_nonneg _
30
31 lemma sqrt_two_add_series_lt_two : ∀(n : ℕ), sqrt_two_add_series 0 n < 2
32 | 0 := by norm_num
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
33 | (n+1) :=
34 begin
35 refine lt_of_lt_of_le _ (le_of_eq $ sqrt_sqr $ le_of_lt two_pos),
src └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
36 rw [sqrt_two_add_series, sqrt_lt],
id └────┘
src └──┘ └┘ └────┘┴
typ └──┘ └┘ └────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────┘└──
37 apply add_lt_of_lt_sub_left,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────────────────┘└─
38 apply lt_of_lt_of_le (sqrt_two_add_series_lt_two n),
id └────────────┘ └────────────────────────┘ ┴
src └────┘└────────────┘┴ ┴ ┴
typ └────┘└────────────┘┴ └────────────────────────┘┴┴┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────┘└─
39 norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num
id └────────┘ └─────────────────────────────┘
src └──────┘ └────┘└────────┘ └──────┘ └────┘└─────────────────────────────┘ └────────
typ └──────┘ └────┘└────────┘ └──────┘ └────┘└─────────────────────────────┘ └────────
doc └──────┘ └────┘ └──────┘ └────┘ └────────
txt └──────┘ └────┘ └──────┘ └────┘ └────────
par └──────┘ └────┘ └──────┘ └────┘ └────────
pid ┴ ┴ └
st ───────────┘└────────────────┘└────────┘└─────────────────────────────────────┘└──────────
40 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
41
42 lemma sqrt_two_add_series_succ (x : ℝ) :
id ┴
src ┴
typ ┴
43 ∀(n : ℕ), sqrt_two_add_series x (n+1) = sqrt_two_add_series (sqrt (2 + x)) n
id ┴ ┴ └─────────────────┘ ┴ ┴┴ ┴ └─────────────────┘ └──┘ ┴ ┴ ┴
src ┴ └─────────────────┘ ┴ ┴ └─────────────────┘ └──┘ ┴
typ ┴ ┴ └─────────────────┘ ┴ ┴┴ ┴ └─────────────────┘ └──┘ ┴ ┴ ┴
doc └─────────────────┘ └─────────────────┘
44 | 0 := rfl
id └─┘
src └─┘
typ └─┘
45 | (n+1) := by rw [sqrt_two_add_series, sqrt_two_add_series_succ, sqrt_two_add_series]
id ┴ └─────────────────┘ └──────────────────────┘ └─────────────────┘
src ┴ └──┘└─────────────────┘└┘ └┘└─────────────────┘└─
typ ┴ └──┘└─────────────────┘└┘└──────────────────────┘└┘└─────────────────┘└─
doc └──┘└─────────────────┘└┘ └┘└─────────────────┘└─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └──────────────────────┘└────────────────────────┘└───────────────────┘┴└
46
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
47 lemma sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
48 ∀(n : ℕ), sqrt_two_add_series x n ≤ sqrt_two_add_series y n
id ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
src ┴ └─────────────────┘ ┴ └─────────────────┘
typ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
doc └─────────────────┘ └─────────────────┘
49 | 0 := h
id ┴
typ ┴
50 | (n+1) :=
id ┴
src ┴
typ ┴
51 begin
st └─────
52 rw [sqrt_two_add_series, sqrt_two_add_series],
id └─────────────────┘ └─────────────────┘
src └──┘└─────────────────┘└┘└─────────────────┘┴
typ └──┘└─────────────────┘└┘└─────────────────┘┴
doc └──┘└─────────────────┘└┘└─────────────────┘┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────────┘└───────────────────┘└──
53 apply sqrt_le_sqrt, apply add_le_add_left, apply sqrt_two_add_series_monotone_left
id └──────────┘ └─────────────┘
src └────┘└──────────┘ └────┘└─────────────┘ └────┘ └
typ └────┘└──────────┘ └────┘└─────────────┘ └────┘ └
doc └────┘ └────┘ └────┘ └
txt └────┘ └────┘ └────┘ └
par └────┘ └────┘ └────┘ └
pid ┴ ┴ ┴ └
st ─────────────────────┘└─────────────────────┘└─────────────────────────────────────────
54 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
55
56 lemma sqrt_two_add_series_step_up {a b n : ℕ} {z : ℝ} (c d : ℕ)
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
57 (hz : sqrt_two_add_series (c/d) n ≤ z) (hb : b ≠ 0) (hd : d ≠ 0)
id └─────────────────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────┘ ┴ ┴ ┴ ┴
typ └─────────────────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────────┘
58 (h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b) : sqrt_two_add_series (a/b) (n+1) ≤ z :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴┴┴ ┴┴ ┴ ┴
doc └─────────────────┘
59 begin
st └─────
60 refine le_trans _ hz, rw [sqrt_two_add_series_succ], apply sqrt_two_add_series_monotone_left,
id └──────┘ └┘ └──────────────────────┘ └───────────────────────────────┘
src └─────┘└──────┘└─┘ └──┘└──────────────────────┘┴ └────┘└───────────────────────────────┘
typ └─────┘└──────┘└─┘└┘ └──┘└──────────────────────┘┴ └────┘└───────────────────────────────┘
doc └─────┘ └─┘ └──┘ ┴ └────┘
txt └─────┘ └─┘ └──┘ ┴ └────┘
par └─────┘ └─┘ └──┘ ┴ └────┘
pid ┴ └─┘ └┘ ┴ ┴
st ─────────────────────┘└────────────────────────────┘└────────────────────────────────────────┘└─
61 rwa [sqrt_le_left, div_pow, add_div_eq_mul_add_div, div_le_iff, mul_comm (_/_), ←mul_div_assoc,
id └──────────┘ └─────┘ └────────────────────┘ └────────┘ └──────┘ ┴ └───────────┘
src └───┘└──────────┘└┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘┴ ┴┴└───┘└───────────┘└─
typ └───┘└──────────┘└┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘┴ ┴┴└───┘└───────────┘└─
doc └───┘ └┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
txt └───┘ └┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
par └───┘ └┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
pid └┘ └┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
st ──────────────────┘└───────┘└──────────────────────┘└──────────┘└──────────────┘└──────────────┘└─
62 le_div_iff, ←nat.cast_pow, ←nat.cast_pow, ←@nat.cast_one ℝ, ←nat.cast_bit0, ←nat.cast_mul,
id └────────┘ └──────────┘ └──────────┘ └──────────┘ └───────────┘ └──────────┘
src ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘┴ └─┘└───────────┘└─┘└──────────┘└─
typ ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘┴ └─┘└───────────┘└─┘└──────────┘└─
doc ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
txt ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
par ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
pid ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
st ───────────────┘└─────────────┘└─────────────┘└────────────────┘└──────────────┘└─────────────┘└─
63 ←nat.cast_mul, ←nat.cast_add, ←nat.cast_mul, nat.cast_le, mul_comm b],
id └──────────┘ └──────────┘ └──────────┘ └─────────┘ └──────┘ ┴
src ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘┴ ┴
typ ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘┴┴┴
doc ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴
txt ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴
par ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴
pid ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴
st ──────────────────┘└─────────────┘└─────────────┘└───────────┘└──────────┘┴└─
64 apply pow_pos, iterate 2 {apply nat.cast_pos.2, apply nat.pos_of_ne_zero, assumption},
id └─────┘ └──────────┘ └────────────────┘
src └────┘└─────┘ └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘┴
typ └────┘└─────┘ └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘┴
doc └────┘ └─────────┘└────┘ └┘└┘└────┘ └┘└────────┘┴
txt └────┘ └─────────┘└────┘ └┘└┘└────┘ └┘└────────┘┴
par └────┘ └─────────┘└────┘ └┘└┘└────┘ └┘└────────┘┴
pid ┴ ┴└───────┘ └────────┘ └───────────┘
st ──────────────┘└───────────────────────────────┘└────────────────────────┘└──────────┘└┘└
65 exact nat.cast_ne_zero.2 hb,
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘
typ └────┘└──────────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ────────────────────────────┘└─
66 exact nat.cast_ne_zero.2 hd,
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘
typ └────┘└──────────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ────────────────────────────┘└─
67 exact div_nonneg (nat.cast_nonneg _) (nat.cast_pos.2 $ nat.pos_of_ne_zero hd)
id └────────┘ └─────────────┘ └──────────┘ └────────────────┘ └┘
src └────┘└────────┘┴ └─────────────┘└──┘ └──────────┘└─┘ ┴└────────────────┘┴ └┘
typ └────┘└────────┘┴ └─────────────┘└──┘ └──────────┘└─┘ ┴└────────────────┘┴└┘└┘
doc └────┘ ┴ └──┘ └─┘ ┴ ┴ └┘
txt └────┘ ┴ └──┘ └─┘ ┴ ┴ └┘
par └────┘ ┴ └──┘ └─┘ ┴ ┴ └┘
pid ┴ ┴ └──┘ └─┘ ┴ ┴ ┴┴
st ───────────────────────────────────────────────────────────────────────────────┘
68 end
st └─┘
69
70 lemma sqrt_two_add_series_step_down {c d n : ℕ} {z : ℝ} (a b : ℕ)
id ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴
71 (hz : z ≤ sqrt_two_add_series (a/b) n) (hb : b ≠ 0) (hd : d ≠ 0)
id ┴ ┴ └─────────────────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────────────────┘ ┴ ┴ ┴
typ ┴ ┴ └─────────────────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────────┘
72 (h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2) : z ≤ sqrt_two_add_series (c/d) (n+1) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴┴┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴┴┴ ┴┴
doc └─────────────────┘
73 begin
st └─────
74 apply le_trans hz, rw [sqrt_two_add_series_succ], apply sqrt_two_add_series_monotone_left,
id └──────┘ └┘ └──────────────────────┘ └───────────────────────────────┘
src └────┘└──────┘┴ └──┘└──────────────────────┘┴ └────┘└───────────────────────────────┘
typ └────┘└──────┘┴└┘ └──┘└──────────────────────┘┴ └────┘└───────────────────────────────┘
doc └────┘ ┴ └──┘ ┴ └────┘
txt └────┘ ┴ └──┘ ┴ └────┘
par └────┘ ┴ └──┘ ┴ └────┘
pid ┴ ┴ └┘ ┴ ┴
st ──────────────────┘└────────────────────────────┘└────────────────────────────────────────┘└─
75 apply le_sqrt_of_sqr_le,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────┘└─
76 rwa [div_pow, add_div_eq_mul_add_div, div_le_iff, mul_comm (_/_), ←mul_div_assoc,
id └─────┘ └────────────────────┘ └────────┘ └──────┘ ┴ └───────────┘
src └───┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘┴ ┴┴└───┘└───────────┘└─
typ └───┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘┴ ┴┴└───┘└───────────┘└─
doc └───┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
txt └───┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
par └───┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
pid └┘ └┘ └┘ └┘ ┴ ┴ └───┘ └─
st ─────────────┘└──────────────────────┘└──────────┘└──────────────┘└──────────────┘└─
77 le_div_iff, ←nat.cast_pow, ←nat.cast_pow, ←@nat.cast_one ℝ, ←nat.cast_bit0, ←nat.cast_mul,
id └────────┘ └──────────┘ └──────────┘ └──────────┘ └───────────┘ └──────────┘
src ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘┴ └─┘└───────────┘└─┘└──────────┘└─
typ ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘┴ └─┘└───────────┘└─┘└──────────┘└─
doc ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
txt ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
par ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
pid ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘ └─
st ───────────────┘└─────────────┘└─────────────┘└────────────────┘└──────────────┘└─────────────┘└─
78 ←nat.cast_mul, ←nat.cast_add, ←nat.cast_mul, nat.cast_le, mul_comm (b ^ 2)],
id └──────────┘ └──────────┘ └──────────┘ └─────────┘ └──────┘ ┴ ┴
src ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘┴ ┴┴└──┘
typ ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘┴ ┴┴┴└──┘
doc ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴ └──┘
txt ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴ └──┘
par ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴ └──┘
pid ──────┘ └─┘ └─┘ └┘ └┘ ┴ ┴ └──┘
st ──────────────────┘└─────────────┘└─────────────┘└───────────┘└────────────────┘┴└─
79 swap, apply pow_pos, iterate 2 {apply nat.cast_pos.2, apply nat.pos_of_ne_zero, assumption},
id └─────┘ └──────────┘ └────────────────┘
src └──┘ └────┘└─────┘ └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘┴
typ └──┘ └────┘└─────┘ └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘┴
doc └──┘ └────┘ └─────────┘└────┘ └┘└┘└────┘ └┘└────────┘┴
txt └──┘ └────┘ └─────────┘└────┘ └┘└┘└────┘ └┘└────────┘┴
par └──┘ └────┘ └─────────┘└────┘ └┘└┘└────┘ └┘└────────┘┴
pid ┴ ┴└───────┘ └────────┘ └───────────┘
st ─────┘└─────────────┘└───────────────────────────────┘└────────────────────────┘└──────────┘└┘└
80 exact nat.cast_ne_zero.2 hd,
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘
typ └────┘└──────────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ────────────────────────────┘└─
81 exact nat.cast_ne_zero.2 hb
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘ ┴
typ └────┘└──────────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────────┘
82 end
st └─┘
83
84 @[simp] lemma cos_pi_over_two_pow : ∀(n : ℕ), cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2
id ┴ ┴ └─┘ └┘ ┴ ┴ ┴┴ ┴ └─────────────────┘ ┴ ┴
src ┴ └─┘ └┘ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
typ ┴ ┴ └─┘ └┘ ┴ ┴ ┴┴ ┴ └─────────────────┘ ┴ ┴
doc └──┘ └┘ └─────────────────┘
85 | 0 := by simp
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
86 | (n+1) :=
id ┴
src ┴
typ ┴
87 begin
st └─────
88 symmetry, rw [div_eq_iff_mul_eq], symmetry,
id └───────────────┘
src └──────┘ └──┘└───────────────┘┴ └──────┘
typ └──────┘ └──┘└───────────────┘┴ └──────┘
doc └──────┘ └──┘ ┴ └──────┘
txt └──────┘ └──┘ ┴ └──────┘
par └──────┘ └──┘ ┴ └──────┘
pid └┘ ┴
st ───────────┘└─────────────────────┘└─────────┘└─
89 rw [sqrt_two_add_series, sqrt_eq_iff_sqr_eq, mul_pow, cos_square, ←mul_div_assoc,
id └─────────────────┘ └────────────────┘ └─────┘ └────────┘ └───────────┘
src └──┘└─────────────────┘└┘└────────────────┘└┘└─────┘└┘└────────┘└─┘└───────────┘└─
typ └──┘└─────────────────┘└┘└────────────────┘└┘└─────┘└┘└────────┘└─┘└───────────┘└─
doc └──┘└─────────────────┘└┘ └┘ └┘ └─┘ └─
txt └──┘ └┘ └┘ └┘ └─┘ └─
par └──┘ └┘ └┘ └┘ └─┘ └─
pid └┘ └┘ └┘ └┘ └─┘ └─
st ──────────────────────────┘└──────────────────┘└───────┘└──────────┘└──────────────┘└─
90 nat.add_succ, pow_succ, mul_div_mul_left, cos_pi_over_two_pow, add_mul],
id └──────────┘ └──────┘ └──────────────┘ └─────────────────┘ └─────┘
src ─────┘└──────────┘└┘└──────┘└┘└──────────────┘└┘ └┘└─────┘┴
typ ─────┘└──────────┘└┘└──────┘└┘└──────────────┘└┘└─────────────────┘└┘└─────┘┴
doc ─────┘ └┘ └┘ └┘ └┘ ┴
txt ─────┘ └┘ └┘ └┘ └┘ ┴
par ─────┘ └┘ └┘ └┘ └┘ ┴
pid ─────┘ └┘ └┘ └┘ └┘ ┴
st ─────────────────┘└────────┘└────────────────┘└───────────────────┘└───────┘└──
91 congr, norm_num,
src └───┘ └──────┘
typ └───┘ └──────┘
doc └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
st ────────┘└────────┘└─
92 rw [mul_comm, pow_two, mul_assoc, ←mul_div_assoc, mul_div_cancel_left, ←mul_div_assoc,
id └──────┘ └─────┘ └───────┘ └───────────┘ └─────────────────┘ └───────────┘
src └──┘└──────┘└┘└─────┘└┘└───────┘└─┘└───────────┘└┘└─────────────────┘└─┘└───────────┘└─
typ └──┘└──────┘└┘└─────┘└┘└───────┘└─┘└───────────┘└┘└─────────────────┘└─┘└───────────┘└─
doc └──┘ └┘ └┘ └─┘ └┘ └─┘ └─
txt └──┘ └┘ └┘ └─┘ └┘ └─┘ └─
par └──┘ └┘ └┘ └─┘ └┘ └─┘ └─
pid └┘ └┘ └┘ └─┘ └┘ └─┘ └─
st ───────────────┘└───────┘└─────────┘└──────────────┘└───────────────────┘└──────────────┘└─
93 mul_div_cancel_left],
id └─────────────────┘
src ───────┘└─────────────────┘┴
typ ───────┘└─────────────────┘┴
doc ───────┘ ┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ──────────────────────────┘└──
94 norm_num, norm_num, apply pow_ne_zero, norm_num, norm_num,
id └─────────┘
src └──────┘ └──────┘ └────┘└─────────┘ └──────┘ └──────┘
typ └──────┘ └──────┘ └────┘└─────────┘ └──────┘ └──────┘
doc └──────┘ └──────┘ └────┘ └──────┘ └──────┘
txt └──────┘ └──────┘ └────┘ └──────┘ └──────┘
par └──────┘ └──────┘ └────┘ └──────┘ └──────┘
pid ┴
st ───────────┘└────────┘└─────────────────┘└────────┘└────────┘└─
95 apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num,
id └────────┘ └─────────────────────────────┘
src └────┘└────────┘ └──────┘ └────┘└─────────────────────────────┘ └──────┘
typ └────┘└────────┘ └──────┘ └────┘└─────────────────────────────┘ └──────┘
doc └────┘ └──────┘ └────┘ └──────┘
txt └────┘ └──────┘ └────┘ └──────┘
par └────┘ └──────┘ └────┘ └──────┘
pid ┴ ┴
st ───────────────────┘└────────┘└─────────────────────────────────────┘└────────┘└─
96 apply le_of_lt, apply mul_pos, apply cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two,
id └──────┘ └─────┘ └───────────────────────────────────────────┘
src └────┘└──────┘ └────┘└─────┘ └────┘└───────────────────────────────────────────┘
typ └────┘└──────┘ └────┘└─────┘ └────┘└───────────────────────────────────────────┘
doc └────┘ └────┘ └────┘
txt └────┘ └────┘ └────┘
par └────┘ └────┘ └────┘
pid ┴ ┴ ┴
st ─────────────────┘└─────────────┘└───────────────────────────────────────────────────┘└─
97 { transitivity (0 : ℝ), rw neg_lt_zero, apply pi_div_two_pos,
id └─────────┘ └────────────┘
src └───────────┘ └──┘ ┴ └─┘└─────────┘ └────┘└────────────┘
typ └───────────┘ └──┘ ┴ └─┘└─────────┘ └────┘└────────────┘
doc └───────────┘ └──┘ ┴ └─┘ └────┘
txt └───────────┘ └──┘ ┴ └─┘ └────┘
par └───────────┘ └──┘ ┴ └─┘ └────┘
pid ┴ └──┘ ┴ ┴ ┴
st ─────┘└──────────────────┘└──────────────┘└────────────────────┘└─
98 apply div_pos pi_pos, apply pow_pos, norm_num },
id └─────┘ └────┘ └─────┘
src └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
typ └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
doc └────┘ ┴ └────┘ └───────┘
txt └────┘ ┴ └────┘ └───────┘
par └────┘ ┴ └────┘ └───────┘
pid ┴ ┴ ┴ ┴
st ─────────────────────────┘└─────────────┘└─────────┘└┘└
99 apply div_lt_div' (le_refl pi) _ pi_pos _,
id └─────────┘ └─────┘ └┘ └────┘
src └────┘└─────────┘┴ └─────┘┴└┘└──┘└────┘└┘
typ └────┘└─────────┘┴ └─────┘┴└┘└──┘└────┘└┘
doc └────┘ ┴ ┴└┘└──┘ └┘
txt └────┘ ┴ ┴ └──┘ └┘
par └────┘ ┴ ┴ └──┘ └┘
pid ┴ ┴ ┴ └──┘ └┘
st ────────────────────────────────────────────┘└─
100 refine lt_of_le_of_lt (le_of_eq (pow_one _).symm) _,
id └────────────┘ └──────┘ └─────┘
src └─────┘└────────────┘┴ └──────┘┴ └─────┘└─────────┘
typ └─────┘└────────────┘┴ └──────┘┴ └─────┘└─────────┘
doc └─────┘ ┴ ┴ └─────────┘
txt └─────┘ ┴ ┴ └─────────┘
par └─────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ └─────────┘
st ──────────────────────────────────────────────────────┘└─
101 apply pow_lt_pow, norm_num, apply nat.succ_lt_succ, apply nat.succ_pos, all_goals {norm_num}
id └────────┘ └──────────────┘ └──────────┘
src └────┘└────────┘ └──────┘ └────┘└──────────────┘ └────┘└──────────┘ └─────────┘└──────┘└─
typ └────┘└────────┘ └──────┘ └────┘└──────────────┘ └────┘└──────────┘ └─────────┘└──────┘└─
doc └────┘ └──────┘ └────┘ └────┘ └─────────┘└──────┘└─
txt └────┘ └──────┘ └────┘ └────┘ └─────────┘└──────┘└─
par └────┘ └──────┘ └────┘ └────┘ └─────────┘└──────┘└─
pid ┴ ┴ ┴ └─────────┘└
st ───────────────────┘└────────┘└──────────────────────┘└──────────────────┘└───────────┘└──────┘┴└
102 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
103
104 lemma sin_square_pi_over_two_pow (n : ℕ) :
id ┴
src ┴
typ ┴
105 sin (pi / 2 ^ (n+1)) ^ 2 = 1 - (sqrt_two_add_series 0 n / 2) ^ 2 :=
id └─┘ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
src └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
typ └─┘ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
doc └┘ └─────────────────┘
st ┴
106 by rw [sin_square, cos_pi_over_two_pow]
id └────────┘ └─────────────────┘
src └──┘└────────┘└┘└─────────────────┘└─
typ └──┘└────────┘└┘└─────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └─────────────┘└───────────────────┘┴└
107
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
108 lemma sin_square_pi_over_two_pow_succ (n : ℕ) :
id ┴
src ┴
typ ┴
109 sin (pi / 2 ^ (n+2)) ^ 2 = 1 / 2 - sqrt_two_add_series 0 n / 4 :=
id └─┘ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
src └─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴
typ └─┘ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴
doc └┘ └─────────────────┘
110 begin
st └─────
111 rw [sin_square_pi_over_two_pow, sqrt_two_add_series, div_pow, sqr_sqrt, add_div, ←sub_sub],
id └────────────────────────┘ └─────────────────┘ └─────┘ └──────┘ └─────┘ └─────┘
src └──┘└────────────────────────┘└┘└─────────────────┘└┘└─────┘└┘└──────┘└┘└─────┘└─┘└─────┘┴
typ └──┘└────────────────────────┘└┘└─────────────────┘└┘└─────┘└┘└──────┘└┘└─────┘└─┘└─────┘┴
doc └──┘ └┘└─────────────────┘└┘ └┘ └┘ └─┘ ┴
txt └──┘ └┘ └┘ └┘ └┘ └─┘ ┴
par └──┘ └┘ └┘ └┘ └┘ └─┘ ┴
pid └┘ └┘ └┘ └┘ └┘ └─┘ ┴
st ───────────────────────────────┘└───────────────────┘└───────┘└────────┘└───────┘└────────┘└──
112 congr, norm_num, norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg,
id └────────┘ └─────────────────────────────┘
src └───┘ └──────┘ └──────┘ └────┘└────────┘ └──────┘ └────┘└─────────────────────────────┘
typ └───┘ └──────┘ └──────┘ └────┘└────────┘ └──────┘ └────┘└─────────────────────────────┘
doc └──────┘ └──────┘ └────┘ └──────┘ └────┘
txt └───┘ └──────┘ └──────┘ └────┘ └──────┘ └────┘
par └───┘ └──────┘ └──────┘ └────┘ └──────┘ └────┘
pid ┴ ┴
st ──────┘└────────┘└────────┘└────────────────┘└────────┘└─────────────────────────────────────┘└─
113 norm_num
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────┘
114 end
st └─┘
115
116 @[simp] lemma sin_pi_over_two_pow_succ (n : ℕ) :
id ┴
src ┴
typ ┴
doc └──┘
117 sin (pi / 2 ^ (n+2)) = sqrt (2 - sqrt_two_add_series 0 n) / 2 :=
id └─┘ └┘ ┴ ┴ ┴┴ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴
src └─┘ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─────────────────┘ ┴
typ └─┘ └┘ ┴ ┴ ┴┴ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴
doc └┘ └─────────────────┘
118 begin
st └─────
119 symmetry, rw [div_eq_iff_mul_eq], symmetry,
id └───────────────┘
src └──────┘ └──┘└───────────────┘┴ └──────┘
typ └──────┘ └──┘└───────────────┘┴ └──────┘
doc └──────┘ └──┘ ┴ └──────┘
txt └──────┘ └──┘ ┴ └──────┘
par └──────┘ └──┘ ┴ └──────┘
pid └┘ ┴
st ─────────┘└─────────────────────┘└─────────┘└─
120 rw [sqrt_eq_iff_sqr_eq, mul_pow, sin_square_pi_over_two_pow_succ, sub_mul],
id └────────────────┘ └─────┘ └─────────────────────────────┘ └─────┘
src └──┘└────────────────┘└┘└─────┘└┘└─────────────────────────────┘└┘└─────┘┴
typ └──┘└────────────────┘└┘└─────┘└┘└─────────────────────────────┘└┘└─────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ───────────────────────┘└───────┘└───────────────────────────────┘└───────┘└──
121 { congr, norm_num, rw [mul_comm], convert mul_div_cancel' _ _, norm_num, norm_num },
id └──────┘ └─────────────┘
src └───┘ └──────┘ └──┘└──────┘┴ └──────┘└─────────────┘└──┘ └──────┘ └───────┘
typ └───┘ └──────┘ └──┘└──────┘┴ └──────┘└─────────────┘└──┘ └──────┘ └───────┘
doc └──────┘ └──┘ ┴ └──────┘ └──┘ └──────┘ └───────┘
txt └───┘ └──────┘ └──┘ ┴ └──────┘ └──┘ └──────┘ └───────┘
par └───┘ └──────┘ └──┘ ┴ └──────┘ └──┘ └──────┘ └───────┘
pid └┘ ┴ ┴ └──┘ ┴
st ───┘└───┘└────────┘└────────────┘└────────────────────────────┘└────────┘└─────────┘└┘└
122 { rw [sub_nonneg], apply le_of_lt, apply sqrt_two_add_series_lt_two },
id └────────┘ └──────┘ └────────────────────────┘
src └──┘└────────┘┴ └────┘└──────┘ └────┘└────────────────────────┘┴
typ └──┘└────────┘┴ └────┘└──────┘ └────┘└────────────────────────┘┴
doc └──┘ ┴ └────┘ └────┘ ┴
txt └──┘ ┴ └────┘ └────┘ ┴
par └──┘ ┴ └────┘ └────┘ ┴
pid └┘ ┴ ┴ ┴ ┴
st ───┘└────────────┘└───────────────┘└─────────────────────────────────┘└┘└
123 apply le_of_lt, apply mul_pos, apply sin_pos_of_pos_of_lt_pi,
id └──────┘ └─────┘ └─────────────────────┘
src └────┘└──────┘ └────┘└─────┘ └────┘└─────────────────────┘
typ └────┘└──────┘ └────┘└─────┘ └────┘└─────────────────────┘
doc └────┘ └────┘ └────┘
txt └────┘ └────┘ └────┘
par └────┘ └────┘ └────┘
pid ┴ ┴ ┴
st ───────────────┘└─────────────┘└─────────────────────────────┘└─
124 { apply div_pos pi_pos, apply pow_pos, norm_num },
id └─────┘ └────┘ └─────┘
src └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
typ └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
doc └────┘ ┴ └────┘ └───────┘
txt └────┘ ┴ └────┘ └───────┘
par └────┘ ┴ └────┘ └───────┘
pid ┴ ┴ ┴ ┴
st ───┘└──────────────────┘└─────────────┘└─────────┘└┘└
125 refine lt_of_lt_of_le _ (le_of_eq (div_one _)), rw [div_lt_div_left],
id └────────────┘ └──────┘ └─────┘ └─────────────┘
src └─────┘└────────────┘└─┘ └──────┘┴ └─────┘└──┘ └──┘└─────────────┘┴
typ └─────┘└────────────┘└─┘ └──────┘┴ └─────┘└──┘ └──┘└─────────────┘┴
doc └─────┘ └─┘ ┴ └──┘ └──┘ ┴
txt └─────┘ └─┘ ┴ └──┘ └──┘ ┴
par └─────┘ └─┘ ┴ └──┘ └──┘ ┴
pid ┴ └─┘ ┴ └──┘ └┘ ┴
st ───────────────────────────────────────────────┘└───────────────────┘└──
126 refine lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _,
id └────────────┘ └──────┘ └──────┘
src └─────┘└────────────┘┴ └──────┘┴ └──────┘└─────────┘
typ └─────┘└────────────┘┴ └──────┘┴ └──────┘└─────────┘
doc └─────┘ ┴ ┴ └─────────┘
txt └─────┘ ┴ ┴ └─────────┘
par └─────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ └─────────┘
st ─────────────────────────────────────────────────────┘└─
127 apply pow_lt_pow, norm_num, apply nat.succ_pos, apply pi_pos,
id └────────┘ └──────────┘ └────┘
src └────┘└────────┘ └──────┘ └────┘└──────────┘ └────┘└────┘
typ └────┘└────────┘ └──────┘ └────┘└──────────┘ └────┘└────┘
doc └────┘ └──────┘ └────┘ └────┘
txt └────┘ └──────┘ └────┘ └────┘
par └────┘ └──────┘ └────┘ └────┘
pid ┴ ┴ ┴
st ─────────────────┘└────────┘└──────────────────┘└────────────┘└─
128 apply pow_pos, all_goals {norm_num}
id └─────┘
src └────┘└─────┘ └─────────┘└──────┘└┘
typ └────┘└─────┘ └─────────┘└──────┘└┘
doc └────┘ └─────────┘└──────┘└┘
txt └────┘ └─────────┘└──────┘└┘
par └────┘ └─────────┘└──────┘└┘
pid ┴ └─────────┘┴
st ──────────────┘└───────────┘└──────┘┴┴
129 end
st └─┘
130
131 lemma cos_pi_div_four : cos (pi / 4) = sqrt 2 / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴
doc └┘
132 by { transitivity cos (pi / 2 ^ 2), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
133
134 lemma sin_pi_div_four : sin (pi / 4) = sqrt 2 / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴
doc └┘
135 by { transitivity sin (pi / 2 ^ 2), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
136
137 lemma cos_pi_div_eight : cos (pi / 8) = sqrt (2 + sqrt 2) / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴
doc └┘
138 by { transitivity cos (pi / 2 ^ 3), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
139
140 lemma sin_pi_div_eight : sin (pi / 8) = sqrt (2 - sqrt 2) / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴
doc └┘
141 by { transitivity sin (pi / 2 ^ 3), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
142
143 lemma cos_pi_div_sixteen : cos (pi / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
doc └┘
144 by { transitivity cos (pi / 2 ^ 4), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
145
146 lemma sin_pi_div_sixteen : sin (pi / 16) = sqrt (2 - sqrt (2 + sqrt 2)) / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
doc └┘
147 by { transitivity sin (pi / 2 ^ 4), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
148
149 lemma cos_pi_div_thirty_two : cos (pi / 32) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
doc └┘
150 by { transitivity cos (pi / 2 ^ 5), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
151
152 lemma sin_pi_div_thirty_two : sin (pi / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
id └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
src └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
typ └─┘ └┘ ┴ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴ └──┘ ┴
doc └┘
153 by { transitivity sin (pi / 2 ^ 5), congr, norm_num, simp }
id └─┘ └┘ ┴ ┴
src └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
typ └───────────┘└─┘┴ └┘┴┴└─┘┴└─┘ └───┘ └──────┘ └───┘
doc └───────────┘ ┴ └┘┴ └─┘ └─┘ └──────┘ └───┘
txt └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
par └───────────┘ ┴ ┴ └─┘ └─┘ └───┘ └──────┘ └───┘
pid ┴ ┴ ┴ └─┘ └─┘ ┴
st └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
154
155 lemma pi_gt_sqrt_two_add_series (n : ℕ) : pi > 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) :=
id ┴ └┘ ┴ ┴ ┴┴ ┴ └──┘ ┴ └─────────────────┘ ┴
src ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─────────────────┘
typ ┴ └┘ ┴ ┴ ┴┴ ┴ └──┘ ┴ └─────────────────┘ ┴
doc └┘ └─────────────────┘
156 begin
st └─────
157 have : pi > sqrt (2 - sqrt_two_add_series 0 n) / 2 * 2 ^ (n+2),
id └┘ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴┴
src └─────┘└┘┴┴┴└──┘┴ └┘┴┴└─────────────────┘└─┘ └┘┴└─┘┴└─┘┴┴ ┴└┘
typ └─────┘└┘┴┴┴└──┘┴ └┘┴┴└─────────────────┘└─┘ └┘┴└─┘┴└─┘┴┴ ┴┴└┘
doc └─────┘└┘┴ ┴ ┴ └┘ ┴└─────────────────┘└─┘ └┘ └─┘ └─┘ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ └─┘ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ └─┘ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ └─┘ ┴ └┘
st ───────────────────────────────────────────────────────────────┘└─
158 { apply mul_lt_of_lt_div, apply pow_pos, norm_num,
id └──────────────┘ └─────┘
src └────┘└──────────────┘ └────┘└─────┘ └──────┘
typ └────┘└──────────────┘ └────┘└─────┘ └──────┘
doc └────┘ └────┘ └──────┘
txt └────┘ └────┘ └──────┘
par └────┘ └────┘ └──────┘
pid ┴ ┴
st ───┘└────────────────────┘└─────────────┘└────────┘└─
159 rw [←sin_pi_over_two_pow_succ], apply sin_lt, apply div_pos pi_pos, apply pow_pos, norm_num },
id └──────────────────────┘ └────┘ └─────┘ └────┘ └─────┘
src └───┘└──────────────────────┘┴ └────┘└────┘ └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
typ └───┘└──────────────────────┘┴ └────┘└────┘ └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
doc └───┘ ┴ └────┘ └────┘ ┴ └────┘ └───────┘
txt └───┘ ┴ └────┘ └────┘ ┴ └────┘ └───────┘
par └───┘ ┴ └────┘ └────┘ ┴ └────┘ └───────┘
pid └─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────┘└─────────────┘└────────────────────┘└─────────────┘└─────────┘└┘└
160 apply lt_of_le_of_lt (le_of_eq _) this,
id └────────────┘ └──────┘ └──┘
src └────┘└────────────┘┴ └──────┘└──┘
typ └────┘└────────────┘┴ └──────┘└──┘└──┘
doc └────┘ ┴ └──┘
txt └────┘ ┴ └──┘
par └────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ───────────────────────────────────────┘└─
161 rw [pow_succ _ (n+1), ←mul_assoc, div_mul_cancel, mul_comm], norm_num
id └──────┘ ┴ └───────┘ └────────────┘ └──────┘
src └──┘└──────┘└─┘ └───┘└───────┘└┘└────────────┘└┘└──────┘┴ └───────┘
typ └──┘└──────┘└─┘ ┴ └───┘└───────┘└┘└────────────┘└┘└──────┘┴ └───────┘
doc └──┘ └─┘ └───┘ └┘ └┘ ┴ └───────┘
txt └──┘ └─┘ └───┘ └┘ └┘ ┴ └───────┘
par └──┘ └─┘ └───┘ └┘ └┘ ┴ └───────┘
pid └┘ └─┘ └───┘ └┘ └┘ ┴ ┴
st ─────────────────────┘└──────────┘└──────────────┘└────────┘└──────────┘
162 end
st └─┘
163
164 lemma pi_lt_sqrt_two_add_series (n : ℕ) :
id ┴
src ┴
typ ┴
165 pi < 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) + 1 / 4 ^ n :=
id └┘ ┴ ┴ ┴┴ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴ ┴
typ └┘ ┴ ┴ ┴┴ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └─────────────────┘
166 begin
st └─────
167 have : pi < (sqrt (2 - sqrt_two_add_series 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n+2),
id └┘ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└┘┴┴┴ └──┘┴ └┘┴┴└─────────────────┘└─┘ └┘┴└─┘┴└─┘ ┴ └┘┴┴ └┘ └─┘ └──┘┴└─┘ ┴ └┘
typ └─────┘└┘┴┴┴ └──┘┴ └┘┴┴└─────────────────┘└─┘ └┘┴└─┘┴└─┘ ┴ └┘┴┴ └┘ └─┘ └──┘┴└─┘ ┴ ┴ └┘
doc └─────┘└┘┴ ┴ ┴ └┘ ┴└─────────────────┘└─┘ └┘ └─┘ └─┘ ┴ └┘ ┴ └┘ └─┘ └──┘ └─┘ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ └─┘ ┴ └┘ ┴ └┘ └─┘ └──┘ └─┘ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ └─┘ ┴ └┘ ┴ └┘ └─┘ └──┘ └─┘ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ └─┘ └─┘ ┴ └┘ ┴ └┘ └─┘ └──┘ └─┘ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
168 { rw [←div_lt_iff, ←sin_pi_over_two_pow_succ],
id └────────┘ └──────────────────────┘
src └───┘└────────┘└─┘└──────────────────────┘┴
typ └───┘└────────┘└─┘└──────────────────────┘┴
doc └───┘ └─┘ ┴
txt └───┘ └─┘ ┴
par └───┘ └─┘ ┴
pid └─┘ └─┘ ┴
st ───┘└─────────────┘└─────────────────────────┘└──
169 refine lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _,
id └────────────┘ └────────────────────┘ └─────────────┘
src └─────┘└────────────┘┴ └────────────────────┘┴ └─────────────┘└──────┘
typ └─────┘└────────────┘┴ └────────────────────┘┴ └─────────────┘└──────┘
doc └─────┘ ┴ ┴ └──────┘
txt └─────┘ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └──────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
170 { apply div_pos pi_pos, apply pow_pos, norm_num },
id └─────┘ └────┘ └─────┘
src └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
typ └────┘└─────┘┴└────┘ └────┘└─────┘ └───────┘
doc └────┘ ┴ └────┘ └───────┘
txt └────┘ ┴ └────┘ └───────┘
par └────┘ ┴ └────┘ └───────┘
pid ┴ ┴ ┴ ┴
st ─────┘└──────────────────┘└─────────────┘└─────────┘└┘└
171 { apply div_le_of_le_mul, apply pow_pos, norm_num, refine le_trans pi_le_four _,
id └──────────────┘ └─────┘ └──────┘ └────────┘
src └────┘└──────────────┘ └────┘└─────┘ └──────┘ └─────┘└──────┘┴└────────┘└┘
typ └────┘└──────────────┘ └────┘└─────┘ └──────┘ └─────┘└──────┘┴└────────┘└┘
doc └────┘ └────┘ └──────┘ └─────┘ ┴ └┘
txt └────┘ └────┘ └──────┘ └─────┘ ┴ └┘
par └────┘ └────┘ └──────┘ └─────┘ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘
st ─────┘└────────────────────┘└─────────────┘└────────┘└────────────────────────────┘└─
172 simp only [show ((4 : ℝ) = 2 ^ 2), by norm_num, mul_one],
id ┴ └─────┘
src └─────────┘ ┴ └──┘ └┘┴└─┘ └──────┘└──────┘└┘└─────┘┴
typ └─────────┘ ┴ └──┘ └┘┴└─┘ └──────┘└──────┘└┘└─────┘┴
doc └─────────┘ ┴ └──┘ └┘ └─┘ └──────┘└──────┘└┘ ┴
txt └─────────┘ ┴ └──┘ └┘ └─┘ └──────┘└──────┘└┘ ┴
par └─────────┘ ┴ └──┘ └┘ └─┘ └──────┘└──────┘└┘ ┴
pid ┴└──┘└┘ ┴ └──┘ └┘ └─┘ └────────────────┘ ┴
st ──────────────────────────────────────────┘└───────┘└────────┘└─
173 apply pow_le_pow, norm_num, apply le_add_of_nonneg_left, apply nat.zero_le },
id └────────┘ └───────────────────┘ └─────────┘
src └────┘└────────┘ └──────┘ └────┘└───────────────────┘ └────┘└─────────┘┴
typ └────┘└────────┘ └──────┘ └────┘└───────────────────┘ └────┘└─────────┘┴
doc └────┘ └──────┘ └────┘ └────┘ ┴
txt └────┘ └──────┘ └────┘ └────┘ ┴
par └────┘ └──────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────┘└────────┘└───────────────────────────┘└──────────────────┘└┘└
174 apply add_le_add_left, rw div_le_div_right,
id └─────────────┘ └──────────────┘
src └────┘└─────────────┘ └─┘└──────────────┘
typ └────┘└─────────────┘ └─┘└──────────────┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ ┴
st ────────────────────────┘└───────────────────┘└─
175 apply le_div_of_mul_le, apply pow_pos, apply pow_pos, norm_num,
id └──────────────┘ └─────┘ └─────┘
src └────┘└──────────────┘ └────┘└─────┘ └────┘└─────┘ └──────┘
typ └────┘└──────────────┘ └────┘└─────┘ └────┘└─────┘ └──────┘
doc └────┘ └────┘ └────┘ └──────┘
txt └────┘ └────┘ └────┘ └──────┘
par └────┘ └────┘ └────┘ └──────┘
pid ┴ ┴ ┴
st ─────────────────────────┘└─────────────┘└─────────────┘└────────┘└─
176 rw [←mul_pow],
id └─────┘
src └───┘└─────┘┴
typ └───┘└─────┘┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ───────────────┘└──
177 refine le_trans _ (le_of_eq (one_pow 3)), apply pow_le_pow_of_le_left,
id └──────┘ └──────┘ └─────┘ └───────────────────┘
src └─────┘└──────┘└─┘ └──────┘┴ └─────┘└──┘ └────┘└───────────────────┘
typ └─────┘└──────┘└─┘ └──────┘┴ └─────┘└──┘ └────┘└───────────────────┘
doc └─────┘ └─┘ ┴ └──┘ └────┘
txt └─────┘ └─┘ ┴ └──┘ └────┘
par └─────┘ └─┘ ┴ └──┘ └────┘
pid ┴ └─┘ ┴ └──┘ ┴
st ───────────────────────────────────────────┘└───────────────────────────┘└─
178 { apply le_of_lt, apply mul_pos, apply div_pos pi_pos, apply pow_pos, norm_num, apply pow_pos,
id └──────┘ └─────┘ └─────┘ └────┘ └─────┘ └─────┘
src └────┘└──────┘ └────┘└─────┘ └────┘└─────┘┴└────┘ └────┘└─────┘ └──────┘ └────┘└─────┘
typ └────┘└──────┘ └────┘└─────┘ └────┘└─────┘┴└────┘ └────┘└─────┘ └──────┘ └────┘└─────┘
doc └────┘ └────┘ └────┘ ┴ └────┘ └──────┘ └────┘
txt └────┘ └────┘ └────┘ ┴ └────┘ └──────┘ └────┘
par └────┘ └────┘ └────┘ ┴ └────┘ └──────┘ └────┘
pid ┴ ┴ ┴ ┴ ┴ ┴
st ─────┘└────────────┘└─────────────┘└────────────────────┘└─────────────┘└────────┘└─────────────┘└─
179 norm_num },
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴
st ──────────────┘└┘└
180 apply mul_le_of_le_div, apply pow_pos, norm_num,
id └──────────────┘ └─────┘
src └────┘└──────────────┘ └────┘└─────┘ └──────┘
typ └────┘└──────────────┘ └────┘└─────┘ └──────┘
doc └────┘ └────┘ └──────┘
txt └────┘ └────┘ └──────┘
par └────┘ └────┘ └──────┘
pid ┴ ┴
st ─────────────────────────┘└─────────────┘└────────┘└─
181 refine le_trans ((div_le_div_right _).mpr pi_le_four) _, apply pow_pos, norm_num,
id └──────┘ └──────────────┘ └────────┘ └─────┘
src └─────┘└──────┘┴ └──────────────┘└──────┘└────────┘└─┘ └────┘└─────┘ └──────┘
typ └─────┘└──────┘┴ └──────────────┘└──────┘└────────┘└─┘ └────┘└─────┘ └──────┘
doc └─────┘ ┴ └──────┘ └─┘ └────┘ └──────┘
txt └─────┘ ┴ └──────┘ └─┘ └────┘ └──────┘
par └─────┘ ┴ └──────┘ └─┘ └────┘ └──────┘
pid ┴ ┴ └──────┘ └─┘ ┴
st ──────────────────────────────────────────────────────────┘└─────────────┘└────────┘└─
182 rw [pow_succ, pow_succ, ←mul_assoc, ←field.div_div_eq_div_mul],
id └──────┘ └──────┘ └───────┘ └──────────────────────┘
src └──┘└──────┘└┘└──────┘└─┘└───────┘└─┘└──────────────────────┘┴
typ └──┘└──────┘└┘└──────┘└─┘└───────┘└─┘└──────────────────────┘┴
doc └──┘ └┘ └─┘ └─┘ ┴
txt └──┘ └┘ └─┘ └─┘ ┴
par └──┘ └┘ └─┘ └─┘ ┴
pid └┘ └┘ └─┘ └─┘ ┴
st ───────────────┘└────────┘└──────────┘└─────────────────────────┘└──
183 convert le_refl _, norm_num, norm_num, apply pow_ne_zero, norm_num, norm_num,
id └─────┘ └─────────┘
src └──────┘└─────┘└┘ └──────┘ └──────┘ └────┘└─────────┘ └──────┘ └──────┘
typ └──────┘└─────┘└┘ └──────┘ └──────┘ └────┘└─────────┘ └──────┘ └──────┘
doc └──────┘ └┘ └──────┘ └──────┘ └────┘ └──────┘ └──────┘
txt └──────┘ └┘ └──────┘ └──────┘ └────┘ └──────┘ └──────┘
par └──────┘ └┘ └──────┘ └──────┘ └────┘ └──────┘ └──────┘
pid ┴ └┘ ┴
st ────────────────────┘└────────┘└────────┘└─────────────────┘└────────┘└────────┘└─
184 apply pow_pos, norm_num },
id └─────┘
src └────┘└─────┘ └───────┘
typ └────┘└─────┘ └───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ ┴
st ────────────────┘└─────────┘└┘└
185 apply lt_of_lt_of_le this (le_of_eq _), rw [add_mul], congr' 1,
id └────────────┘ └──┘ └──────┘ └─────┘
src └────┘└────────────┘┴ ┴ └──────┘└─┘ └──┘└─────┘┴ └──────┘
typ └────┘└────────────┘┴└──┘┴ └──────┘└─┘ └──┘└─────┘┴ └──────┘
doc └────┘ ┴ ┴ └─┘ └──┘ ┴ └──────┘
txt └────┘ ┴ ┴ └─┘ └──┘ ┴ └──────┘
par └────┘ ┴ ┴ └─┘ └──┘ ┴ └──────┘
pid ┴ ┴ ┴ └─┘ └┘ ┴ ┴┴
st ───────────────────────────────────────┘└───────────┘└─────────┘└─
186 { rw [pow_succ _ (n+1), ←mul_assoc, div_mul_cancel, mul_comm], norm_num },
id └──────┘ ┴ └───────┘ └────────────┘ └──────┘
src └──┘└──────┘└─┘ └───┘└───────┘└┘└────────────┘└┘└──────┘┴ └───────┘
typ └──┘└──────┘└─┘ ┴ └───┘└───────┘└┘└────────────┘└┘└──────┘┴ └───────┘
doc └──┘ └─┘ └───┘ └┘ └┘ ┴ └───────┘
txt └──┘ └─┘ └───┘ └┘ └┘ ┴ └───────┘
par └──┘ └─┘ └───┘ └┘ └┘ ┴ └───────┘
pid └┘ └─┘ └───┘ └┘ └┘ ┴ ┴
st ───┘└──────────────────┘└──────────┘└──────────────┘└────────┘└──────────┘└┘└
187 rw [pow_succ, ←pow_mul, mul_comm n 2, pow_mul, show (2 : ℝ) ^ 2 = 4, by norm_num, pow_succ,
id └──────┘ └─────┘ └──────┘ ┴ └─────┘ ┴ └──────┘
src └──┘└──────┘└─┘└─────┘└┘└──────┘┴ └──┘└─────┘└┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└┘└──────┘└─
typ └──┘└──────┘└─┘└─────┘└┘└──────┘┴┴└──┘└─────┘└┘ ┴ └──┘ └┘ └─┘┴└─────┘└──────┘└┘└──────┘└─
doc └──┘ └─┘ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└┘ └─
txt └──┘ └─┘ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└┘ └─
par └──┘ └─┘ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└┘ └─
pid └┘ └─┘ └┘ ┴ └──┘ └┘ ┴ └──┘ └┘ └─┘ └───────────────┘ └─
st ─────────────┘└────────┘└───────────┘└────────┘└────────────────────────┘└───────┘└────────┘└─
188 pow_succ, ←mul_assoc (2 : ℝ), show (2 : ℝ) * 2 = 4, by norm_num, ←mul_assoc, div_mul_cancel,
id └──────┘ └───────┘ ┴ └───────┘ └────────────┘
src ─────┘└──────┘└─┘└───────┘┴ └──┘ └─┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└─┘└───────┘└┘└────────────┘└─
typ ─────┘└──────┘└─┘└───────┘┴ └──┘ └─┘ ┴ └──┘ └┘ └─┘┴└─────┘└──────┘└─┘└───────┘└┘└────────────┘└─
doc ─────┘ └─┘ ┴ └──┘ └─┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└─┘ └┘ └─
txt ─────┘ └─┘ ┴ └──┘ └─┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└─┘ └┘ └─
par ─────┘ └─┘ ┴ └──┘ └─┘ ┴ └──┘ └┘ └─┘ └─────┘└──────┘└─┘ └┘ └─
pid ─────┘ └─┘ ┴ └──┘ └─┘ ┴ └──┘ └┘ └─┘ └────────────────┘ └┘ └─
st ─────────────┘└──────────────────┘└────────────────────────┘└───────┘└──────────┘└──────────────┘└─
189 mul_comm ((2 : ℝ) ^ n), ←div_div_eq_div_mul, div_mul_cancel],
id └──────┘ ┴ └────────────────┘ └────────────┘
src ─────┘└──────┘┴ └──┘ └┘ ┴ └──┘└────────────────┘└┘└────────────┘┴
typ ─────┘└──────┘┴ └──┘ └┘ ┴┴└──┘└────────────────┘└┘└────────────┘┴
doc ─────┘ ┴ └──┘ └┘ ┴ └──┘ └┘ ┴
txt ─────┘ ┴ └──┘ └┘ ┴ └──┘ └┘ ┴
par ─────┘ ┴ └──┘ └┘ ┴ └──┘ └┘ ┴
pid ─────┘ ┴ └──┘ └┘ ┴ └──┘ └┘ ┴
st ───────────────────────────┘└───────────────────┘└──────────────┘└──
190 apply pow_ne_zero, norm_num, norm_num
id └─────────┘
src └────┘└─────────┘ └──────┘ └───────┘
typ └────┘└─────────┘ └──────┘ └───────┘
doc └────┘ └──────┘ └───────┘
txt └────┘ └──────┘ └───────┘
par └────┘ └──────┘ └───────┘
pid ┴ ┴
st ──────────────────┘└────────┘└─────────┘
191 end
st └─┘
192
193 lemma pi_gt_three : pi > 3 :=
id └┘ ┴
src └┘ ┴
typ └┘ ┴
doc └┘
194 begin
st └─────
195 refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 1), rw [mul_comm],
id └────────────┘ └───────────────────────┘ └──────┘
src └─────┘└────────────┘└─┘ └───────────────────────┘└─┘ └──┘└──────┘┴
typ └─────┘└────────────┘└─┘ └───────────────────────┘└─┘ └──┘└──────┘┴
doc └─────┘ └─┘ └─┘ └──┘ ┴
txt └─────┘ └─┘ └─┘ └──┘ ┴
par └─────┘ └─┘ └─┘ └──┘ ┴
pid ┴ └─┘ └─┘ └┘ ┴
st ──────────────────────────────────────────────────────┘└────────────┘└──
196 apply le_mul_of_div_le, norm_num, apply le_sqrt_of_sqr_le, rw [le_sub],
id └──────────────┘ └───────────────┘ └────┘
src └────┘└──────────────┘ └──────┘ └────┘└───────────────┘ └──┘└────┘┴
typ └────┘└──────────────┘ └──────┘ └────┘└───────────────┘ └──┘└────┘┴
doc └────┘ └──────┘ └────┘ └──┘ ┴
txt └────┘ └──────┘ └────┘ └──┘ ┴
par └────┘ └──────┘ └────┘ └──┘ ┴
pid ┴ ┴ └┘ ┴
st ───────────────────────┘└────────┘└───────────────────────┘└──────────┘└──
197 rw show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div],
id ┴ ┴ └───────────┘ └──────┘
src └─┘ ┴ └┘ └┘┴┴ └┘ ┴┴ └┘ └────────┘└───────────┘└┘└──────┘┴
typ └─┘ ┴ └┘ └┘┴┴ └┘ ┴┴ └┘ └────────┘└───────────┘└┘└──────┘┴
doc └─┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ ┴
txt └─┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ ┴
par └─┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ ┴
pid ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ ┴
st ────────────────────────────────┘└────────────────┘└────────┘┴└─
198 apply sqrt_two_add_series_step_up 23 16,
id └─────────────────────────┘
src └────┘└─────────────────────────┘└────┘
typ └────┘└─────────────────────────┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ └──┘└┘
st ────────────────────────────────────────┘└─
199 all_goals {norm_num}
src └─────────┘└──────┘└┘
typ └─────────┘└──────┘└┘
doc └─────────┘└──────┘└┘
txt └─────────┘└──────┘└┘
par └─────────┘└──────┘└┘
pid └─────────┘┴
st ────────────┘└──────┘┴┴
200 end
st └─┘
201
202 lemma pi_gt_314 : pi > 3.14 :=
id └┘ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴
doc └┘
203 begin
st └─────
204 refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 4), rw [mul_comm],
id └────────────┘ └───────────────────────┘ └──────┘
src └─────┘└────────────┘└─┘ └───────────────────────┘└─┘ └──┘└──────┘┴
typ └─────┘└────────────┘└─┘ └───────────────────────┘└─┘ └──┘└──────┘┴
doc └─────┘ └─┘ └─┘ └──┘ ┴
txt └─────┘ └─┘ └─┘ └──┘ ┴
par └─────┘ └─┘ └─┘ └──┘ ┴
pid ┴ └─┘ └─┘ └┘ ┴
st ──────────────────────────────────────────────────────┘└────────────┘└──
205 apply le_mul_of_div_le, norm_num, apply le_sqrt_of_sqr_le,
id └──────────────┘ └───────────────┘
src └────┘└──────────────┘ └──────┘ └────┘└───────────────┘
typ └────┘└──────────────┘ └──────┘ └────┘└───────────────┘
doc └────┘ └──────┘ └────┘
txt └────┘ └──────┘ └────┘
par └────┘ └──────┘ └────┘
pid ┴ ┴
st ───────────────────────┘└────────┘└───────────────────────┘└─
206 rw [le_sub, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
id └────┘ ┴ ┴ └───────────┘ └──────┘
src └──┘└────┘└┘ ┴ └┘ └┘┴┴ └┘ ┴┴ └┘ └────────┘└───────────┘└┘└──────┘└┘
typ └──┘└────┘└┘ ┴ └┘ └┘┴┴ └┘ ┴┴ └┘ └────────┘└───────────┘└┘└──────┘└┘
doc └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
txt └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
par └──┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
pid └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
st ───────────┘└────────────────────────────┘└────────────────┘└────────┘┴└──
207 apply sqrt_two_add_series_step_up 99 70,
id └─────────────────────────┘
src └────┘└─────────────────────────┘└────┘
typ └────┘└─────────────────────────┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ └──┘└┘
st ────────────────────────────────────────┘└─
208 apply sqrt_two_add_series_step_up 874 473,
id └─────────────────────────┘
src └────┘└─────────────────────────┘└──────┘
typ └────┘└─────────────────────────┘└──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └───┘└─┘
st ──────────────────────────────────────────┘└─
209 apply sqrt_two_add_series_step_up 1940 989,
id └─────────────────────────┘
src └────┘└─────────────────────────┘└───────┘
typ └────┘└─────────────────────────┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └────┘└─┘
st ───────────────────────────────────────────┘└─
210 apply sqrt_two_add_series_step_up 1447 727,
id └─────────────────────────┘
src └────┘└─────────────────────────┘└───────┘
typ └────┘└─────────────────────────┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └────┘└─┘
st ───────────────────────────────────────────┘└─
211 all_goals {norm_num}
src └─────────┘└──────┘└┘
typ └─────────┘└──────┘└┘
doc └─────────┘└──────┘└┘
txt └─────────┘└──────┘└┘
par └─────────┘└──────┘└┘
pid └─────────┘┴
st ────────────┘└──────┘┴┴
212 end
st └─┘
213
214 lemma pi_lt_315 : pi < 3.15 :=
id └┘ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴
doc └┘
215 begin
st └─────
216 refine lt_of_lt_of_le (pi_lt_sqrt_two_add_series 4) _,
id └────────────┘ └───────────────────────┘
src └─────┘└────────────┘┴ └───────────────────────┘└───┘
typ └─────┘└────────────┘┴ └───────────────────────┘└───┘
doc └─────┘ ┴ └───┘
txt └─────┘ ┴ └───┘
par └─────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ──────────────────────────────────────────────────────┘└─
217 apply add_le_of_le_sub_right, rw [mul_comm], apply mul_le_of_le_div, apply pow_pos, norm_num,
id └────────────────────┘ └──────┘ └──────────────┘ └─────┘
src └────┘└────────────────────┘ └──┘└──────┘┴ └────┘└──────────────┘ └────┘└─────┘ └──────┘
typ └────┘└────────────────────┘ └──┘└──────┘┴ └────┘└──────────────┘ └────┘└─────┘ └──────┘
doc └────┘ └──┘ ┴ └────┘ └────┘ └──────┘
txt └────┘ └──┘ ┴ └────┘ └────┘ └──────┘
par └────┘ └──┘ ┴ └────┘ └────┘ └──────┘
pid ┴ └┘ ┴ ┴ ┴
st ─────────────────────────────┘└────────────┘└───────────────────────┘└─────────────┘└────────┘└─
218 rw [sqrt_le_left, sub_le, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
id └──────────┘ └────┘ ┴ ┴ └───────────┘ └──────┘
src └──┘└──────────┘└┘└────┘└┘ ┴ └┘ └┘┴┴ └┘ ┴┴ └┘ └────────┘└───────────┘└┘└──────┘└┘
typ └──┘└──────────┘└┘└────┘└┘ ┴ └┘ └┘┴┴ └┘ ┴┴ └┘ └────────┘└───────────┘└┘└──────┘└┘
doc └──┘ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
txt └──┘ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
par └──┘ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
pid └┘ └┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ └────────┘ └┘ └┘
st ─────────────────┘└──────┘└────────────────────────────┘└────────────────┘└────────┘┴└──
219 apply sqrt_two_add_series_step_down 140 99,
id └───────────────────────────┘
src └────┘└───────────────────────────┘└─────┘
typ └────┘└───────────────────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └───┘└┘
st ───────────────────────────────────────────┘└─
220 apply sqrt_two_add_series_step_down 279 151,
id └───────────────────────────┘
src └────┘└───────────────────────────┘└──────┘
typ └────┘└───────────────────────────┘└──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └───┘└─┘
st ────────────────────────────────────────────┘└─
221 apply sqrt_two_add_series_step_down 51 26,
id └───────────────────────────┘
src └────┘└───────────────────────────┘└────┘
typ └────┘└───────────────────────────┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ └──┘└┘
st ──────────────────────────────────────────┘└─
222 apply sqrt_two_add_series_step_down 412 207,
id └───────────────────────────┘
src └────┘└───────────────────────────┘└──────┘
typ └────┘└───────────────────────────┘└──────┘
doc └────┘ └──────┘
txt └────┘ └──────┘
par └────┘ └──────┘
pid ┴ └───┘└─┘
st ────────────────────────────────────────────┘└─
223 all_goals {norm_num}
src └─────────┘└──────┘└┘
typ └─────────┘└──────┘└┘
doc └─────────┘└──────┘└┘
txt └─────────┘└──────┘└┘
par └─────────┘└──────┘└┘
pid └─────────┘┴
st ────────────┘└──────┘┴┴
224 end
st └─┘
225
226 /- A computation of the first 7 digits of pi is given here:
227 <https://gist.github.com/fpvandoorn/5b405988bc2e61953d56e3597db16ecf>
228 This is not included in mathlib, because of slow compilation time.
229 -/
230
231 end real